T:Type, R:(TT).
(a, b:T. Dec(a = b))
 (a, b:T. Dec(R(a,b)))
 Linorder(T;a,b.R(a,b))
 (L:(T List). L':T List. (sorted-by(R;L') & no_repeats(T;L') & L  L' & L'  L)) 

latex

Definitions

x:A  B(x), type List, {x:A| B(x)} , sorted-by(R;L), no_repeats(T;l), A  B, Type, Linorder(T;x,y.R(x;y)), x,y. t(x;y), P  Q, Dec(P), , f(a), b, P  Q, x:A. B(x), s = t, P & Q, , x:AB(x), x:A. B(x), P  Q, [d], x.A(x), t  T, Order(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), <a, b>, left + right, P  Q, A, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , (x  l), ||as||, a < b, False, A  B, i  j < k, , {i..j}, Void, l[i], xL. P(x), #$n

Lemmas

int seg wf, select wf, linorder functionality wrt iff, rev implies wf, connex wf, order wf, sorted-by-exists, bool wf, iff wf, assert wf, dcdr-to-bool-equivalence, decidable wf, linorder wf, l contains wf, no repeats wf, sorted-by wf